/*
 *  SimplifyRES.java
 * 
 *  Copyright (C) 2012-2013 Sylvain Lamprier, Tewfik Ziaidi, Lom Messan Hillah and Nicolas Baskiotis
 * 
 *  This file is part of CARE.
 * 
 *   CARE is free software: you can redistribute it and/or modify
 *   it under the terms of the GNU General Public License as published by
 *   the Free Software Foundation, either version 3 of the License, or
 *   (at your option) any later version.
 *
 *   CARE is distributed in the hope that it will be useful,
 *   but WITHOUT ANY WARRANTY; without even the implied warranty of
 *   MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 *   GNU General Public License for more details.
 *
 *   You should have received a copy of the GNU General Public License
 *   along with CARE.  If not, see <http://www.gnu.org/licenses/>.
 */

package regexp.fromFSA;


import regexp.Regexp;
import regexp.fromFSA.Equation;
import regexp.fromFSA.EquationSystem;
public class SimplifyRES {

	public EquationSystem transform(EquationSystem from) {
		EquationSystem sys = from;

		int loopcount = 0; // avoid infinite loops
		
		//System.out.println("Original system size: " + sys.getEquation().size());
		//RegexpUtil.printSys(sys);//TODO
		while(!isSimplified(sys)) {//TODO 1000	 && loopcount++ < 2000	
			Equation eq = getTrivialEquation(sys);
			while (eq != null) {//if (eq != null) {//
				eq.setRight(new NormalizeRegexp().simplyNormalize(eq.getRight()));
				sys = (EquationSystem) new ReplaceEquation().transform(sys, eq);
				//normalizeAllEquations(sys);//No!!!
				//RegexpUtil.printSys(sys);
				eq = getTrivialEquation(sys);
			}
			//System.out.println("===========================");
			//RegexpUtil.printSys(sys);
			
			Equation eq2 = getNonTrivialSolvableEquation(sys);
			if(eq2 != null) {//if(eq2 != null) {//
				sys = applyLemma(sys, eq2);
				sys.getContainsTable().get(eq2.getLeft()).remove(eq2.getLeft());
				//normalizeAllEquations(sys);
				//RegexpUtil.printSys(sys);//TODO
				//eq2 = getNonTrivialSolvableEquation(sys);
			}
						
			//normalizeAllEquations(sys);//TODO no need to normalized all, just normalize the replaced one
			loopcount++;
			//System.out.println("==loopcount: " + loopcount + "  equation size: " + sys.getEquation().size());//TODO
			//RegexpUtil.printSys(sys);//TODO
		}
		//TODO
		//System.out.println("IS THIS SYS EQUATION SIMPLIFIED? "+isSimplified(sys));
		normalizeAllEquations(sys);
		RegexpExtractionUtils.printSys(sys);
		
		return sys;
	}

	private void normalizeAllEquations(EquationSystem sys) {
		for (Equation eq : sys.getEquation()) {
			eq.setRight((Regexp) new NormalizeRegexp()
					.transform(eq.getRight()));
		}
	}

	private EquationSystem applyLemma(EquationSystem sys, Equation eq) {		
		
		for (Equation eq0 : sys.getEquation()) {
			if (eq.getLeft().equals(eq0.getLeft())) {
				//eq0.setRight(new NormalizeRegexp().transform(eq0.getRight()));
				Equation newEq = (Equation) new ApplyLemmaToEquation().transform(eq0);
				//eq0.setRight(new NormalizeRegexp().transform(newEq.getRight()));
				break;
			}
		}
		
		return sys;		
	}

	private boolean isSimplified(EquationSystem sys) {
		return sys.getEquation().size() == 1
				&& getNonTrivialSolvableEquation(sys) == null
				&& getTrivialEquation(sys) == null;
	}

	/**
	 * get the equation which is contained by itself
	 **/
	private Equation getNonTrivialSolvableEquation(EquationSystem sys) {//TODO REWRITE
		for (Equation eq : sys.getEquation()) {
			if (RegexpExtractionUtils.eqContainsVariable(sys, eq, eq.getLeft())) {
				//System.out.println("GOTTA NON-TRIVIAL E: ");// + eq.getLeft().getName());
				return eq;
			}
		}
		return null;
	}

	/**
	 * get the equation which is NOT contained by itself
	 **/
	private Equation getTrivialEquation(EquationSystem sys) {//DONE
		for (Equation eq : sys.getEquation()) {
			// we don't want to lose the objective variable!!
			if (!eq.getLeft().equals(sys.getObjective())
					&& !RegexpExtractionUtils.eqContainsVariable(sys, eq, eq.getLeft())) {
				//System.out.println("GOTTA TRIVIAL E");
				return eq;
			}
		}
		return null;
	}
	
	

}
